Inference at * 1 
Iof proof for Lemma eq int eq false elim sqequal:



1. i : 
2. j : 
  ((i = j) ~ ff)  i  j 

latex

 by D 0 

latex

 1: 

 1: 3. (i = j) ~ ff
 1:   i  j
 2: .....wf..... NILNIL

 2:   ((i = j) ~ ff)  Type
 .

Definitions	P  Q, t  T
Lemmas	nequal wf